Focus the state machine on the rejected call - #158

Description

Closes #117.

When the State Machine view is opened from a state refinement error, it marks the rejected call on the full diagram. There are two sets of states:

• P, the states the receiver can be in, from Found;
• A, the states the call accepts, from Expected.

The view marks:

• Invalid, P \ A: red outline and ✕. The call fails from here.
• Valid, P ∩ A: green outline and ✓. The call is fine from here.
• Accepted but not possible here, A \ P: a thin dashed yellow outline and no text. It hints at where the object could be brought.
• The failed method: every arrow labelled with it gets a red label, including inside merged labels. The rejected call is never drawn as a new transition.

Red and green have a faint fill and yellow is outline only, so a large machine stays calm.

The full diagram is always shown. Focus mode dims what does not help with the error:

• states outside P ∪ A;
• constructors;
• every method name that is neither the failed method nor a transition that moves the receiver out of a state in P to a different state. This applies to each name inside merged labels: in getOption / receive / send / … only receive stays bright.

An arrow's path is dimmed only when all of its names are. "Show all" and "Focus on error" switch the dimming off and on and keep pan and zoom. The label text is identical in both modes, so the layout does not move.

A one-line legend shows only the marks that are present: "✕ Call rejected", "✓ Call allowed" and "Allowed, but not reachable here". In light themes the dashed outline uses a darker warning colour.

One summary line sits above the diagram, e.g. "socket.receive() is rejected when socket is in state closed · allowed in state bound".

Edge cases

• When the receiver's state is unknown (every state is possible), only A is marked, and the summary says the state is unknown.
• With no known receiver or accepted states, or with an older server, the view behaves as on main.

Data

• P is possibleStates (Add the receiver's possible states to the error context liquidjava-fsm#11). With an older server, it falls back to definiteFoundState and then actualStates.
• A is expectedStates.
• Dependency: bumps liquidjava-fsm to 0.1.5.
• The call is matched by its exact method name from the error context, not by label text.
• "Copy Mermaid Source" copies the plain diagram.

Screenshots

These are real verifier output in headless VS Code.

UDP chat client. The study example E_OSS_A1_22_UdpChatClient: receive after an if that may close the socket. In focus mode the following stay bright:

• receive;
• close and connect out of bound;
• the accessors out of closed.

The accessors stay bright because the DatagramSocket spec writes from = "closed(this) && connected(old(this))", which is drawn as an arrow from closed to connected. That old(...) in a from is a spec error, not an extension issue.

Whole UDP machine: focus in dark and light, and Show all

DefaultMutableTreeNode (the issue's example). getFirstChild() after removeAllChildren():

• childrenAllowed is invalid;
• maybeHasChildren is accepted;
• add, the way there, stays bright;
• removeAllChildren is dimmed.

Dimmed unrelated state (simplified demo machine, not a real class)

Tests

Run against liquidjava-fsm 0.1.5 and verifier 0.0.35 from Maven Central:

• npm run lint and npm run test:typecheck: clean.
• npm run test:unit: 75 passed in 7 files.
• npm test (VS Code): 8 + 1 passing.
• Server mvn test: 24 passing.
• Local smoke test: passed.

The new tests cover:

• the split into Valid, Invalid and accepted states;
• the fallbacks and the unknown-state case;
• empty or unknown states;
• exact method matching (receive does not match receiveAll);
• red labels inside merged labels;
• dimming of rendered paths and labels, per-name dimming inside merged labels, and the rule for which methods count as useful;
• the legend;
• dimmed constructors;
• diagram clipping below the summary when panned;
• the toggle keeping zoom;
• plain Mermaid copy;
• the computed outline styles.

Independently reviewed twice; all findings were fixed.

Known limits

• Large machines such as DatagramSocket have long stacked self-loop labels. This already happens on main.
• Show state errors in the State Machine view #159 touches the same webview files; whichever PR merges second will be rebased.

🤖 Generated with Claude Code